T:Type, A,B:(T List), x,y:T.
l_before(x; y; append(A; B); T)
 (l_before(x; y; A; T)  l_before(x; y; B; T)  ((x  A)  (y  B))) 

latex

Definitions	x:A. B(x), t  T, P  Q, append(as; bs), P  Q, P  Q, Y, P  Q, P  Q, prop{i:l}, guard(T), x. t(x), False, x(s)
Lemmas	l before wf, l member wf, nil before, nil member, all functionality wrt iff, iff wf, append wf, iff functionality wrt iff, or functionality wrt iff, and functionality wrt iff, cons member, cons before, member append